Background
Basic concepts
equivalences in/of -categories
Universal constructions
Local presentation
Theorems
Extra stuff, structure, properties
Models
(2,1)-quasitopos?
structures in a cohesive (∞,1)-topos
The notion of an elementary (∞,1)-topos is an analogue of the notion of elementary topos in (∞,1)-category theory. This is in contrast to the notion of a Grothendieck (∞,1)-topos equivalent to an (∞,1)-category of (∞,1)-sheaves, the analogue of a sheaf topos, which is more specific (see geometric homotopy type theory).
Note that every Grothendieck (∞,1)-topos provides categorical semantics for homotopy type theory with univalent types of types and also higher inductive types (HITs) – see here. Elementary -toposes ought to be roughly the larger class of all -categories that provide categorical semantics for such homotopy type theory. More precisely, we will define an elementary -topos to have the -categorical structure that ought to correspond to that type-theoretic structure; a coherence theorem making it actually model the corresponding type theory is still unknown (but see at initiality conjecture).
In general, the problem with “elementary-izing” the notion of -topos is that Grothendieck -toposes have many properties that are not reflected in type theory due to the finitary nature of type theory; the question is to find appropriate “finitary shadows” of them. For instance, one can construct initial algebras for endofunctors using a transfinite induction argument; thus in type theory we postulate the existence of inductive types. Deciding what class of “infinitary constructions” that are available in Grothendieck -toposes can be described finitarily by something that deserves the name “higher inductive type” is overall an open question, but we can obtain reasonable definitions by restricting the class of HITs we ask for.
There are at least two ambiguities in the above sketch of a definition based on type theory: what exactly do we assume of the universes (object classifiers), and what general class of HITs do we ask for? One reasonable answer to the universe question is that every object should be contained in a universe closed under all the relevant operations, and one reasonable answer to the HITs question is just the non-recursive ones. This leads to the following definition.
An elementary -topos is an -category such that
has finite limits and colimits
There exists a subobject classifier (an object classifier that classifies the collection of all monomorphisms in an (∞,1)-category)
For any morphism in , there exists an object classifier in classifying a class of morphisms that (1) includes and (2) is closed under fiberwise finite limits and colimits, composition (i.e. dependent sums), and dependent products.
Note that this definition is “impredicative” just like an elementary topos, in that it has a classifier for all subobjects. We can’t categorify this to a classifier for all objects due to size paradoxes; the existence of “enough” object classifiers closed under all the basic operations is the “next best thing”. We will refer to an object classifier satisfying (2) above as a universe.
It is reasonable to hope for a coherence theorem showing that any elementary -topos in the above sense admits a model of homotopy type theory with non-recursive HITs (corresponding to the finite colimits), univalent universes (perhaps only weakly Tarski ones), and propositional resizing. See, for instance, model of type theory in an (infinity,1)-topos and relation between type theory and category theory – Univalent homotopy type theory and infinity-toposes.
In an elementary 1-topos we can construct finite colimits and dependent exponentials from non-dependent exponentials and the subobject classifier (or equivalently from power objects). In the -case this seems less likely to be true, since subobjects tell us less about objects that are not 0-truncated. However, there is still a good deal of extra structure that “comes for free” from the above definition.
The initial object of is strict, i.e. any morphism is an equivalence.
Just as for 1-categories, this is true in any cartesian closed -category. For if there is a morphism then the projection has a section , so that is a retract of ; but by cartesian closedness since has a right adjoint and hence preserves colimits.
Binary coproducts in are disjoint, i.e. the injections and are monic, and their pullback is initial.
This is also just like a corresponding proof for 1-toposes (see toposes are extensive). Define and to make the following squares pullbacks:
Specifically, is the kernel pair of . In particular, there is an induced diagonal such that . On the other hand, since is locally cartesian closed, pullback preserves colimits, so is a coproduct diagram. Thus, the pair of morphisms and factor (uniquely) through some , so that in particular . Thus, has both a left and a right inverse, so it is an equivalence, and hence is monic. Dually, is monic.
Now we claim that any two morphisms with domain are equivalent. For the pair of morphisms and factor uniquely through (which, recall, is the coproduct ). But since is an equivalence, this factorization must be (equivalent to) the left coprojection . Therefore, the composite is equivalent to the composite , and similarly so is the composite . Since is monic by the previous paragraph, .
Finally, since is a strict initial object, is monic. And of course is also monic, and these two monomorphisms are classified by two maps into the subobject classifier. By the previous paragraph, , hence and is initial.
In fact, disjoint binary coproducts can actually be constructed from local cartesian closure and the subobject classifier; see FreyRasekh. This is similar to the fact that the finite colimits in an elementary topos can be constructed from the rest of the structure, but it is unclear whether it can be generalized beyond coproducts in the infinite-dimensional case. In particular, it is shown in FreyRasekh that local cartesian closure and the subobject classifier do not suffice to construct pushouts; the -category of truncated spaces is a counterexample.
For any finite family of morphisms , there exists a universe classifying all the .
Since is the pullback of along the injection (this follows from extensivity), a universe classifying must also classify each .
In particular, we have “universe cumulativity”:
For any universe , there is a universe that classifies both and .
All finite colimits are van Kampen.
Since is locally cartesian closed, all colimits are pullback-stable, so it suffices to show descent. Suppose is a finite simplicial set and are colimiting cones under diagrams , and let be a natural transformation whose restriction is equifibered. Let be a universe classifying for each vertex . Then is the pullback of along a cocone , yielding a cocone in which is equifibered.
Since is colimiting under , we have an induced map , where is the cocone vertex. But since colimits are pullback-stable, the pullback of along is a colimiting cocone under , and hence isomorphic to . Thus, is equifibered.
There exists a natural numbers object.
Intuitively, it seems as if (which can be constructed using finite limits and colimits) ought to be the integers and we should be able to construct the natural numbers from it; but it is unclear to the authors of this page how to do that. Instead, we can (using the impredicative subobject classifier) define the smallest subobject of an object classifier that contains the initial object and is closed under taking coproducts with the terminal object. This is almost right, but it is not 0-truncated. We could 0-truncate it, but to get a universal property relative to all objects rather than only 0-truncated ones, we can instead impose structure making the objects rigid, such as a partial order or a graph. This argument is formalized in type theory here; to be precise either it would have to be translated manually into category-theoretic language, or the above conjecture about interpreting type theory in an elementary -topos would have to be proven.
There is an (n-connected, n-truncated) factorization system.
The case can be constructed impredicatively using the subobject classifier: internally, is the smallest truth value implied by . Then we can induct on external natural numbers, defining to be the -image of the composite , where the second map is the -truncation. Note that in general it “goes up a universe level”, so that the -truncation “goes up universe levels”. However, unlike type theory, an elementary -topos has no globally chosen tower of universes, so this doesn’t literally make sense to say. What we can say is that with this construction, it is not clear whether we can find object classifiers that are closed under the -truncation.
However, (Rijke17) shows (again in type theory) that using finite colimits and the natural numbers, the -truncation can be constructed without raising the universe level. Assuming (as always) that this can be translated into -category theory, it implies that we can find object classifiers closed under the -truncation, and hence (by induction) under the -truncation for all . Moreover, with a natural numbers object this induction can be performed internally, obtaining in particular object classifiers closed under the -truncation for all at once.
It seems likely that the construction of W-types in any elementary 1-topos can be repeated in the -case.
There is some structure that the definition probably does not imply, namely a semantic counterpart of arbitrary recursive higher inductive types, such as arbitrary localization. It is certain that these cannot always be constructed in an elementary 1-topos: for instance, HITs imply that all (even infinitary) algebraic theories have initial algebras, whereas this cannot be proven in ZF without the axiom of choice (under appropriate large cardinal hypotheses). Thus, it seems very unlikely that they can be constructed in an elementary -topos. Moreover, it is even unclear exactly what -categorical structure should correspond to arbitrary higher inductive types, not least because we lack an accepted general definition of an “arbitrary HIT”.
However, although this is an open question, it is arguably not a question about the definition of “elementary -topos”, but some stronger notion, analogous to a stronger notion of 1-topos that lacks an accepted name. Moreover, a great deal of homotopy type theory (including synthetic homotopy theory) can be done with only non-recursive HITs, truncations, and a natural numbers type, and even in the absence of a general coherence theorem any particular result of HoTT could probably be explicitly written down in -categorical language.
Since there is no consensus even on the definition of predicative 1-topos, it seems less likely that there is a definitive answer for a predicative -topos. However, it should probably include at least the following axioms (which as we have seen above, are all true in the impredicative case although not included in the definition):
Note that the stronger universe axiom implies, as above, that finite colimits are van Kampen, and in particular therefore that finite coproducts are disjoint. Instead of strengthening this axiom, we could assume explicitly that finite coproducts are disjoint, and then repeat the proof of descent given above.
(Rasekh21) gives a construction using filter products using which we get a large class of elementary -toposes that aren’t Grothendieck toposes. To be precise Corollary 2.31 in the paper gives the following construction: Suppose we’ve an elementary -topos , and a filter on the subobject classifier of which is product-closed, such that the filter quotient? of the elementary topos of 0-truncated objects is not a Grothendieck topos, then the filter quotient is an elementary -topos that isn’t a Grothendieck -topos. Further, examples for the specific case of filter products are constructed.
Other ideas for the construction of an elementary (∞,1)-topos which is not a Grothendieck (∞,1)-topos also exist in the literature. (cf. Anel 21).
Peter Scholze speculates in this comment on the nCafé that the (∞,1)-category of condensed -groupoids might form a predicative elementary (∞,1)-topos which is not a Grothendieck (∞,1)-topos.
A vague version of the above proposed definition is on the very last slide of
It was elaborated further in
See also
Michael Shulman, Towards elementary infinity-toposes, Vladimir Voevodsky Memorial Conference, IAS, September 2018, talk.
Michael Shulman, Peter Lumsdaine, 2016, Semantics and syntax of higher inductive types, (slides)
André Joyal, What is an elementary higher topos?, talk at Reimagining The Foundations Of Algebraic Topology April 07, 2014 - April 11, 2014_ web video PDF (slides 57-end). This lecture contains a proposed definition that is not an -category but a presentation of one by a model category-like structure; this is closer to the type theory, but further from the intended examples. In particular, there are unresolved coherence questions even as to whether every Grothendieck -topos can be presented by a model in Joyal’s sense (in particular, how strict can a universe be made, and can the natural numbers object be made fibrant). Other than that, the main difference is that Joyal assumes only one fixed universe.
For an alternative definition proven (in Theorem 3.16) to be equivalent to the one given above, see
The construction of -truncations without recursive HITs is in
The construction of natural numbers from propositional resizing and univalence is in
The construction of coproducts from local cartesian closure and the subobject classifier is in
Results holding for elementary (∞,1)-toposes:
Nima Rasekh, Yoneda Lemma for Elementary Higher Toposes, (arXiv:1809.01736)
Nima Rasekh, Every Elementary Higher Topos has a Natural Number Object, Theory and Applications of Categories 37 13 (2021) 337-377. (arXiv:1809.01734, tac:37-13)
Nima Rasekh, Truncations and Blakers-Massey in an Elementary Higher Topos, (arXiv:1812.10527)
Using comprehension schemes to characterize categorical properties of elementary ∞-toposes:
On π-finite homotopy types as a partial analogue of the elementary 1-topos FinSet:
The filter product construction is used to construct elementary (∞,1)-toposes which aren’t Grothendieck (∞,1)-toposes in:
Last revised on June 13, 2023 at 14:24:31. See the history of this page for a list of all contributions to it.